1. Technical Field
The present invention relates to model checking and more particularly to systems and methods for combining stateless and state-based model checking.
2. Description of the Related Art
Bounded and unbounded model checking for verifying embedded software have been shown to scale much better when applied on models represented in first-order logic compared to models represented in propositional logic. Further, high level information can be easily provided succinctly in higher-level logic compared to propositional logic. Even with the higher scalability, there are problems in which each of these methods, i.e., bounded and unbounded model checking, fails to perform within the limited resources. These methods have complementary strengths.
Bounded Model Checking (BMC) explores all the program paths for a given bounded depth using a decision procedure (DP) for un-quantified theory. BNC does not store the program states. Such a state-less approach is good at finding bugs. However, with increasing program depths, the formula size of each BMC instance becomes larger and increasing harder to solve.
Unbounded Model Checking (UMC) symbolically computes program states at a given program point reachable from an initial state, along each program path. UMC computes successive images, where each image step essentially involves quantifications of current program state variables and primary (free) input variables. This is achieved using a decision procedure (DP) for quantified first order theory, which is a computationally more expensive operation than DP for un-quantified theory. As the program states computed at a program control point capture the union of executions of all program paths to the program point, the reachability detection for an error block becomes trivial. Note that as the program state is computed for each program path, there is a potential memory blow up when there are many conditional paths. Further, a separate call to BMC is made to generate the witness trace when the reachability of error block is detected.